Nuprl Lemma : void-list-equality2
11,40
postcript
pdf
x
,
y
:(Void List),
T
:Type.
x
=
y
(
T
List)
latex
Definitions
Void
,
t
T
,
type
List
,
Type
,
s
=
t
,
x
:
A
.
B
(
x
)
,
s
~
t
,
x
:
A
B
(
x
)
,
S
T
Lemmas
void-list-equality
origin
x, y:(Void List), T:Type. x = y 
(T List) x, y:(Void List), T:Type. x = y (T List) Tx:A. B(x)
B(x)
T